es:ES, A, B, P, Q:(E), T, T':Type, R:(TT').
(e:E. (A(e)  B(e))  (valtype(e) r T))
 (e:E. (P(e)  Q(e))  (valtype(e) r T'))
 (e:E. (A(e) & B(e)))
 (e:E. (P(e) & Q(e)))
 (e:E. Dec(P(e)))
 (e:E. Dec(A(e)))
 (f:({e:E| A(e)} {e:E| P(e)} ), g:({e:E| B(e)} {e:E| Q(e)} ).
 (e.A(e) e.f(e) e.P(e)) with R
  (e.B(e) e.g(e) e.Q(e)) with R
  (h:{e:E| A(e)  B(e)} {e:E| P(e)  Q(e)} 
  (((e.A(e)  B(e) e.h(e) e.P(e)  Q(e)) with R
  (& (e:{e:E| A(e)  B(e)} . A(e)  (h(e) = f(e)))
  (& (e:{e:E| A(e)  B(e)} . (A(e))  (h(e) = g(e)))))) 

latex

Definitions

x:A. B(x), x:AB(x), P & Q, x:A. B(x), {x:A| B(x)} , P  Q, P  Q, A, x(s), s = t, E, f(a), {T}, Bij(A;B;f), e c e', (e.P(e) a.f(a) e'.Q(e')) with R, t.1, let x,y = A in B(x;y), Dec(P), False, valtype(e), , EqDecider(T), EOrderAxioms(E; pred?; info), kind(e), type List, Msg(M), , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e', r  s, , x:A  B(x), Knd, kindcase(k; a.f(a); l,t.g(l;t) ), x. t(x), x,y. t(x;y), IdLnk, constant_function(f;A;B), <a, b>, loc(e), b, first(e), suptype(S; T), Type, left + right, S  T, Top, x:A.B(x), Void, Unit, SWellFounded(R(x;y)), pred!(e;e'), , Id, EState(T), t  T, ES, P  Q, case b of inl(x) => s(x) | inr(y) => t(y), tt, ff, x.A(x), if b then t else f fi , True, b, P  Q, A c B, Inj(A;B;f), Surj(A;B;f), T, (e < e'), SQType(T), s ~ t, , val(e)

Lemmas

es-val wf, es-causl wf, es-causle wf, member wf, subtype rel set, bnot wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, false wf, true wf, iff wf, bfalse wf, btrue wf, event system wf, unit wf, top wf, first wf, assert wf, not wf, constant function wf, EState wf, IdLnk wf, kindcase wf, Knd wf, rationals wf, bool wf, qle wf, cless wf, val-axiom wf, nat wf, Msg wf, loc wf, kind wf, Id wf, EOrderAxioms wf, deq wf, es-E wf, es-valtype wf, decidable wf, causal-bijection wf